import java.util.*;
import java.io.*;

class test { 


	public static void main(String args[]) { 
		HashMap KBmap = new HashMap();
		//System.out.println(KBmap.keySet());

		String thisLine;
		ArrayList clauses = new ArrayList();

		// read test case from file
		try {
       			BufferedReader br = new BufferedReader(new FileReader("butter.txt"));
       			while ((thisLine = br.readLine()) != null) { // while loop begins here

         			//System.out.println(thisLine);
				// parse clause line
				int[] test = parseClause(KBmap, thisLine);
				/*for(int i=0; i<5; i++){
					System.out.println(test[i]);
				}*/
				clauses.add(test);



       			} // end while 
     		} // end try
     		catch (IOException e) {
       			System.err.println("Error: " + e);
     		}
		// end test case reading

		//System.out.println(KBmap.keySet());

		boolean b = isSatisfiable(clauses);
		if(b){
			System.out.println("C'est satisfiable.");
		} else {
			System.out.println("N'est-ce pas satisfiable.");
		}
		
	} 

	public static int[] parseClause(HashMap KBmap, String cnfclause) {
		int[] output = new int[20];
		
		String term;
		
		int i = 0;
		int negs = 0;
		int isNeg;
		while(i*6 + negs < cnfclause.length()){
			isNeg = 1;
			if(cnfclause.substring(i*6 + negs, i*6 + negs + 1).compareTo("-") == 0){
				negs++;
				isNeg = -1;
			}
			term = cnfclause.substring(i*3 + negs, i*6+negs+3);
			if(KBmap.containsKey(term)) {
				output[i+1] = isNeg*(((Integer) KBmap.get(term)).intValue() + 1);
			} else {
				KBmap.put(term, new Integer(KBmap.size()));
				output[i+1] = isNeg*(((Integer) KBmap.get(term)).intValue() + 1);
			}
			i++; 
		}
		output[0] = i;
		return output;
	}

	public static boolean isSatisfiable(ArrayList clauses) {
		// requires clauses to be an Array List of int arrays
		// first element of the int array denotes how long the actual clause is, in terms of literals

		int[] model = new int[65]; // 65 since model[0] is unused since I forgot and was too lazy to change it
		for(int i=0; i<65; i++){
			model[i] = -1;
		}

		int claus[]; // a single clause
		for(int i=0; i<clauses.size(); i++){
			claus = (int[])clauses.get(i);
			if(claus[0] == 1) { // unit clause
				if(model[Math.abs(claus[1])] < 0) {
					if(claus[1] > 0)  model[Math.abs(claus[1])] = 1;
					else model[Math.abs(claus[1])] = 0;
				} else { // already assigned unit literal, is there a contradiction? 
					// ...this is probably not actually necessary here but I wrote it so I'm keepin' it
					if(model[Math.abs(claus[1])] == 0 && claus[1] > 0) return false;
					if(model[Math.abs(claus[1])] == 1 && claus[1] < 0) return false;
				}
			}
		}

		return DPLL(clauses, model);


	}

	public static boolean DPLL(ArrayList clauses, int[] model){
		int foundUnknown;
		boolean foundTrue;
		int claus[];
		for(int i=0; i<clauses.size(); i++){
			//System.out.println("Clause check: " + i);
			claus = (int[])clauses.get(i);
			//System.out.println(claus[i]);

			foundUnknown = -1;
			foundTrue = false;
			for(int j = 1; j <= claus[0]; j++){
				if(model[Math.abs(claus[j])] == 1 && claus[j] > 0 || model[Math.abs(claus[j])] == 0 && claus[j] < 0){
					// a true literal has been found
					//System.out.println("True " + j + " " + model[Math.abs(claus[j])]);
					foundTrue = true;
					j = claus[0] + 1; // or break or whatever
				} else if(model[Math.abs(claus[j])] == -1 && foundUnknown < 0) {
					// first unknown found in the literal is remembered
					foundUnknown = j;
				}
			}
			if(foundUnknown < 0 && !foundTrue) { // no unknowns or trues found, so everything false
				/*for(int j=1; j<20; j++){
					System.out.print(model[j] + " ");
				}*/
				//System.out.println("False found, clause " + i);
				return false; 
			}
			if(!foundTrue) { // unknown found, no trues found
				//System.out.println("Unknown " + foundUnknown + " " + claus[foundUnknown]);

				int[] cop = new int[model.length];
				System.arraycopy( model, 0, cop, 0, model.length );

				cop[Math.abs(claus[foundUnknown])] = 1;
				if(DPLL(clauses, cop)) return true;
				cop[Math.abs(claus[foundUnknown])] = 0;
				return DPLL(clauses, cop);
			} // everything true
		}
		/*for(int j=1; j<20; j++){
			System.out.print(model[j] + " ");
		}*/
		return true;
	}
}



